Nuprl Definition : ring_p
13,42
postcript
pdf
IsRing(
T
;
plus
;
zero
;
neg
;
times
;
one
)
== IsGroup(
T
;
plus
;
zero
;
neg
) & IsMonoid(
T
;
times
;
one
) & BiLinear(
T
;
plus
;
times
)
latex
Up
rings
1
Wellformedness Lemmas
ring
p
wf
Definitions
IsGroup(
T
;
op
;
id
;
inv
)
,
P
&
Q
,
IsMonoid(
T
;
op
;
id
)
,
BiLinear(
T
;
pl
;
tm
)
origin